app2(app2(app2(if, true), xs), ys) -> xs
app2(app2(app2(if, false), xs), ys) -> ys
app2(app2(filter, p), nil) -> nil
app2(app2(filter, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs))), app2(app2(filter, p), xs))
↳ QTRS
↳ Non-Overlap Check
app2(app2(app2(if, true), xs), ys) -> xs
app2(app2(app2(if, false), xs), ys) -> ys
app2(app2(filter, p), nil) -> nil
app2(app2(filter, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs))), app2(app2(filter, p), xs))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
app2(app2(app2(if, true), xs), ys) -> xs
app2(app2(app2(if, false), xs), ys) -> ys
app2(app2(filter, p), nil) -> nil
app2(app2(filter, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs))), app2(app2(filter, p), xs))
app2(app2(app2(if, true), x0), x1)
app2(app2(app2(if, false), x0), x1)
app2(app2(filter, x0), nil)
app2(app2(filter, x0), app2(app2(cons, x1), x2))
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs))), app2(app2(filter, p), xs))
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(if, app2(p, x))
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs)))
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(filter, p), xs)
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(cons, x), app2(app2(filter, p), xs))
app2(app2(app2(if, true), xs), ys) -> xs
app2(app2(app2(if, false), xs), ys) -> ys
app2(app2(filter, p), nil) -> nil
app2(app2(filter, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs))), app2(app2(filter, p), xs))
app2(app2(app2(if, true), x0), x1)
app2(app2(app2(if, false), x0), x1)
app2(app2(filter, x0), nil)
app2(app2(filter, x0), app2(app2(cons, x1), x2))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs))), app2(app2(filter, p), xs))
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(if, app2(p, x))
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs)))
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(filter, p), xs)
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(cons, x), app2(app2(filter, p), xs))
app2(app2(app2(if, true), xs), ys) -> xs
app2(app2(app2(if, false), xs), ys) -> ys
app2(app2(filter, p), nil) -> nil
app2(app2(filter, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs))), app2(app2(filter, p), xs))
app2(app2(app2(if, true), x0), x1)
app2(app2(app2(if, false), x0), x1)
app2(app2(filter, x0), nil)
app2(app2(filter, x0), app2(app2(cons, x1), x2))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(filter, p), xs)
app2(app2(app2(if, true), xs), ys) -> xs
app2(app2(app2(if, false), xs), ys) -> ys
app2(app2(filter, p), nil) -> nil
app2(app2(filter, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs))), app2(app2(filter, p), xs))
app2(app2(app2(if, true), x0), x1)
app2(app2(app2(if, false), x0), x1)
app2(app2(filter, x0), nil)
app2(app2(filter, x0), app2(app2(cons, x1), x2))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(p, x)
APP2(app2(filter, p), app2(app2(cons, x), xs)) -> APP2(app2(filter, p), xs)
app2 > filter
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
app2(app2(app2(if, true), xs), ys) -> xs
app2(app2(app2(if, false), xs), ys) -> ys
app2(app2(filter, p), nil) -> nil
app2(app2(filter, p), app2(app2(cons, x), xs)) -> app2(app2(app2(if, app2(p, x)), app2(app2(cons, x), app2(app2(filter, p), xs))), app2(app2(filter, p), xs))
app2(app2(app2(if, true), x0), x1)
app2(app2(app2(if, false), x0), x1)
app2(app2(filter, x0), nil)
app2(app2(filter, x0), app2(app2(cons, x1), x2))